es:ES, l:IdLnk, tg:Id, A:Type.
(e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (es-in-port(es;l;tg)  AbsInterface(A)) 

latex

Definitions

ES, t  T, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), Atom$n, valtype(e), rcv(l,tg), kind(e), E, let x,y = A in B(x;y), inr x , t.1, False, ff, if b then t else f fi , val(e), case b of inl(x) => s(x) | inr(y) => t(y), tag(e), lnk(e), isrcv(e), inl x , b, , P  Q, x.A(x), , a = b, P  Q, {T}, es-in-port(es;l;tg), AbsInterface(A)

Lemmas

all functionality wrt iff, implies functionality wrt iff, assert-eq-knd, subtype rel wf, eq knd wf, ifthenelse wf, it wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, bfalse wf, es-rcv-kind, es-val wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf